Nuprl Lemma : R-Dsys-Rplus
11,40
postcript
pdf
A
,
B
:Top. [[
A
B
]] ~ ([[
A
]]
[[
B
]])
latex
Definitions
t
T
,
case(
R
)Rnone:
none
left
right
:
comb
(
left
;
right
)base(
b
).
base
(
b
)
,
[[
R
]]
,
x
:
A
.
B
(
x
)
Lemmas
top
wf
origin
A, B:Top. [[A 
B]] ~ ([[A]] [[B]]) A, B:Top. [[A B]] ~ ([[A]] [[B]]) 
T right: comb(left;right)base(b). base(b)x:A. B(x)